x <<= y == x << y  (x = y) 

latex

---

clarification:

chain-order-le(es;Sys;chain;x;y) == chain-order(es;Sys;chain;x;y)  (x = y  Id) 

latex

Up	abstract chain replication
Wellformedness Lemmas	chain-order-le wf
Definitions	P  Q, x << y, s = t, Id
FDL editor aliases	chain-order-le